$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it as}$, ${\it bs}$:$T$ List.
\\[0ex]($\forall$$x$:$T$. ($x$ $\in$ list{-}diff(${\it eq}$;${\it as}$;${\it bs}$)) $\Leftrightarrow$ ($x$ $\in$ ${\it as}$) \& $\neg$($x$ $\in$ ${\it bs}$))
\\[0ex]\& (no\_repeats($T$;${\it as}$) $\Rightarrow$ no\_repeats($T$;list{-}diff(${\it eq}$;${\it as}$;${\it bs}$)))